Skip to content

copybutton.js: remove DOCUMENTATION_OPTIONS dead code - #222

Open
gastmaier wants to merge 1 commit into
executablebooks:masterfrom
gastmaier:patch-1
Open

gastmaier wants to merge 1 commit into
executablebooks:masterfrom
gastmaier:patch-1

Conversation

@gastmaier

Copy link
Copy Markdown

Supposedly used for doc_url_root, but also dead code.
Why I care? In my use case I remove DOCUMENTATION_OPTIONS from the built pages.

Supposedly used for doc_url_root, but also dead code.
@josephine-wolf-oberholtzer

Copy link
Copy Markdown

Would also love to see this fixed.

As a workaround until somebody merges this, you can toss the following lines into your conf.py to get it to keep working:

def setup(app):
    app.add_js_file(None, body="window.DOCUMENTATION_OPTIONS = {}", priority=0)

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants